es:ES, m:, f:({0..m}E).
(i:{0..(m - 1)}. (f(i) <loc f(i+1)))  (i:{0..m}, j:{0..i}. (f(j) <loc f(i))) 

latex

Definitions	, t  T, x:A. B(x), A  B, P & Q, i  j < k, P  Q, False, A, {i..j}, (e <loc e'), , E, ES, , i  j , P  Q, Dec(P), {T}, SQType(T), Trans(T;x,y.E(x;y))
Lemmas	es-locl-trans, decidable int equal, ge wf, nat properties, nat wf, event system wf, nat plus wf, es-E wf, int seg wf, es-locl wf, le wf